Nuprl Lemma : comb_for_list_accum_wf
4,23
postcript
pdf
(
T
,
T'
,
l
,
y
,
f
,
z
. list_accum(
x
,
a
.
f
(
x
,
a
);
y
;
l
))
T
,
T'
:Type
(
T
List)
T'
(
T'
T
T'
)
True
T'
latex
Definitions
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
list
accum
wf
,
squash
wf
,
true
wf
origin
T,T',l,y,f,z. list_accum(x,a.f(x,a);y;l)) 
T,T':Type
(T List)T'(T'TT')
TrueT' T,T',l,y,f,z. list_accum(x,a.f(x,a);y;l)) T,T':Type(T List)T'(T'TT')TrueT' T
x:A. B(x)T